SherbyNet - /page/wikibook/entry.mu

Micron Document

<!DOCTYPE html>

<title>Davis–Putnam algorithm</title>

</head>

Davis–Putnam algorithm

</h1>

</header>

In <a href="Logic" title="Logic">logic</a> and <a href="Computer_science" title="Computer science">computer science</a>, the Davis–Putnam algorithm was developed by <a href="Martin_Davis_(mathematician)" title="Martin Davis (mathematician)">Martin Davis</a> and <a href="Hilary_Putnam" title="Hilary Putnam">Hilary Putnam</a> for checking the validity of a <a href="First-order_logic" title="First-order logic">first-order logic</a> formula using a <a href="Resolution_(logic)" title="Resolution (logic)">resolution</a>-based decision procedure for <a href="Propositional_logic" title="Propositional logic">propositional logic</a>. Since the set of valid first-order formulas is <a href="Recursively_enumerable" class="mw-redirect" title="Recursively enumerable">recursively enumerable</a> but not <a href="Recursive_set" class="mw-redirect" title="Recursive set">recursive</a>, there exists no general algorithm to solve this problem. Therefore, the Davis–Putnam algorithm only terminates on valid formulas. Today, the term "Davis–Putnam algorithm" is often used synonymously with the resolution-based propositional decision procedure (Davis–Putnam procedure) that is actually only one of the steps of the original algorithm.

<div class="mw-heading mw-heading2"><h2 id="Overview">Overview</h2></div>

The procedure is based on <a href="Herbrand's_theorem" title="Herbrand's theorem">Herbrand's theorem</a>, which implies that an <a href="Satisfiable" class="mw-redirect" title="Satisfiable">unsatisfiable</a> formula has an unsatisfiable <a href="Ground_instance" class="mw-redirect" title="Ground instance">ground instance</a>, and on the fact that a formula is valid if and only if its negation is unsatisfiable. Taken together, these facts imply that to prove the validity of φ it is enough to prove that a ground instance of ¬φ is unsatisfiable. If φ is not valid, then the search for an unsatisfiable ground instance will not terminate.

The procedure for checking validity of a formula φ roughly consists of these three parts:

<ul><li>put the formula ¬φ in <a href="Prenex" class="mw-redirect" title="Prenex">prenex</a> form and eliminate quantifiers</li>

<li>generate all propositional ground instances, one by one</li>

<li>check if each instance is satisfiable.

<ul><li>If some instance is unsatisfiable, then return that φ is valid. Else continue checking.</li></ul></li></ul>

The last part is a <a href="SAT_solver" title="SAT solver">SAT solver</a> based on <a href="Resolution_(logic)" title="Resolution (logic)">resolution</a> (as seen on the illustration), with an eager use of <a href="Unit_propagation" title="Unit propagation">unit propagation</a> and pure literal elimination (elimination of clauses with variables that occur only positively or only negatively in the formula).

<pre>Algorithm DP SAT solver

Input: A set of clauses Φ.

Output: A Truth Value: true if Φ can be satisfied, false otherwise.

</pre>

<pre>function DP-SAT(Φ)

repeat

// unit propagation:

while Φ contains a unit clause {l} do

for every clause c in Φ that contains l do

Φ ← remove-from-formula(c, Φ);

for every clause c in Φ that contains ¬l do

Φ ← remove-from-formula(c, Φ);

Φ ← add-to-formula(c \ {¬l}, Φ);

// eliminate clauses not in normal form:

for every clause c in Φ that contains both a literal l and its negation ¬l do

Φ ← remove-from-formula(c, Φ);

// pure literal elimination:

while there is a literal l all of which occurrences in Φ have the same polarity do

for every clause c in Φ that contains l do

Φ ← remove-from-formula(c, Φ);

// stopping conditions:

if Φ is empty then

return true;

if Φ contains an empty clause then

return false;

// Davis-Putnam procedure:

pick a literal l that occurs with both polarities in Φ

for every clause c in Φ containing l and every clause n in Φ containing its negation ¬l do

// resolve c with n:

r ← (c \ {l}) ∪ (n \ {¬l});

Φ ← add-to-formula(r, Φ);

for every clause c that contains l or ¬l do

Φ ← remove-from-formula(c, Φ);

</pre>

<ul><li>"←" denotes <a href="Assignment_(computer_science)" title="Assignment (computer science)">assignment</a>. For instance, "largest ← item" means that the value of largest changes to the value of item.</li>

<li>"return" terminates the algorithm and outputs the following value.</li></ul>

</div>

At each step of the SAT solver, the intermediate formula generated is <a href="Equisatisfiable" class="mw-redirect" title="Equisatisfiable">equisatisfiable</a>, but possibly not <a href="Logical_equivalence" title="Logical equivalence">equivalent</a>, to the original formula. The resolution step leads to a worst-case exponential blow-up in the size of the formula.

The <a href="Davis%E2%80%93Putnam%E2%80%93Logemann%E2%80%93Loveland_algorithm" class="mw-redirect" title="Davis–Putnam–Logemann–Loveland algorithm">Davis–Putnam–Logemann–Loveland algorithm</a> is a 1962 refinement of the propositional satisfiability step of the Davis–Putnam procedure which requires only a linear amount of memory in the worst case. It eschews the resolution for the splitting rule: a backtracking algorithm that chooses a literal l, and then recursively checks if a simplified formula with l assigned a true value is satisfiable or if a simplified formula with l assigned false is. It still forms the basis for today's (as of 2015) most efficient complete <a href="SAT_solver" title="SAT solver">SAT solvers</a>.

<ul><li><a href="Herbrandization" title="Herbrandization">Herbrandization</a></li></ul>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite id="CITEREFDavisPutnam,_Hilary1960" class="citation journal cs1">Davis, Martin; Putnam, Hilary (1960). <a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F321033.321034">"A Computing Procedure for Quantification Theory"</a>. <a href="Journal_of_the_ACM" title="Journal of the ACM">Journal of the ACM</a>. 7 (3): 201–215. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F321033.321034">10.1145/321033.321034</a>.</cite></li>

<li><cite id="CITEREFDavisLogemann,_GeorgeLoveland,_Donald1962" class="citation journal cs1">Davis, Martin; Logemann, George; Loveland, Donald (1962). <a rel="nofollow" class="external text" href="http://portal.acm.org/citation.cfm?doid=368273.368557">"A Machine Program for Theorem Proving"</a>. <a href="Communications_of_the_ACM" title="Communications of the ACM">Communications of the ACM</a>. 5 (7): 394–397. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F368273.368557">10.1145/368273.368557</a>. <a href="Hdl_(identifier)" class="mw-redirect" title="Hdl (identifier)">hdl</a>:<a rel="nofollow" class="external text" href="https://hdl.handle.net/2027%2Fmdp.39015095248095">2027/mdp.39015095248095</a>.</cite></li>

<li><cite id="CITEREFR._DechterI._Rish" class="citation conference cs1">R. Dechter; I. Rish. "Directional Resolution: The Davis–Putnam Procedure, Revisited". In J. Doyle and E. Sandewall and P. Torasso (ed.). Principles of Knowledge Representation and Reasoning: Proc. of the Fourth International Conference (KR'94). Kaufmann. pp. 134–145.</cite></li>

<li><cite id="CITEREFJohn_Harrison2009" class="citation book cs1">John Harrison (2009). <a rel="nofollow" class="external text" href="https://archive.org/details/handbookpractica00harr">Handbook of practical logic and automated reasoning</a>. Cambridge University Press. pp. <a rel="nofollow" class="external text" href="https://archive.org/details/handbookpractica00harr/page/n100">79</a>–90. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-521-89957-4</bdi>.</cite></li></ul></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2024-08-05" href="https://en.wikipedia.org/wiki/?title=Davis%E2%80%93Putnam_algorithm&oldid=1238818652">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>